Nuprl Lemma : int-inherence
0,22
postcript
pdf
a
:Atom1,
n
:
.
n
:
>>
a
latex
Definitions
x
:
A
.
B
(
x
)
,
A
,
P
Q
,
t
T
,
x
:
T
>>
a
,
False
,
x
:
A
.
B
(
x
)
,
Prop
Lemmas
atom-free-int
,
inheres
wf
origin
a:Atom1, n:
. 
n:>>a a:Atom1, n:. n:>>a x:A. B(x)A
Q
T
x:A. B(x)